\begin{tabbing}
SESAxioms\=\{i:l\}\+
\\[0ex]($E$; $T$; ${\it pred?}$; ${\it info}$; ${\it when}$; ${\it after}$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=(\=$\forall$$e$:$E$, $l$:IdLnk.\+\+
\\[0ex]$\exists$${\it e'}$:$E$.
\\[0ex]$\forall$${\it e''}$:$E$.
\\[0ex]rcv?(${\it e''}$)
\\[0ex]$\Rightarrow$ sender(${\it e''}$) $=$ $e$
\\[0ex]$\Rightarrow$ link(${\it e''}$) $=$ $l$
\\[0ex]$\Rightarrow$ ${\it e''}$ $=$ ${\it e'}$ $\vee$ ${\it e''}$ $<$ ${\it e'}$ \& loc(${\it e'}$) $=$ destination($l$))
\-\\[0ex]\& \=($\forall$$e$, ${\it e'}$:$E$. loc($e$) $=$ loc(${\it e'}$) $\Rightarrow$ ${\it pred?}$($e$) $=$ ${\it pred?}$(${\it e'}$) $\Rightarrow$ $e$ $=$ ${\it e'}$)\+
\\[0ex]\& SWellFounded(pred!($e$;${\it e'}$))
\\[0ex]\& ($\forall$$e$:$E$. $\neg$first($e$) $\Rightarrow$ loc(pred($e$)) $=$ loc($e$))
\\[0ex]\& ($\forall$$e$:$E$. rcv?($e$) $\Rightarrow$ loc(sender($e$)) $=$ source(link($e$)))
\\[0ex]\& (\=$\forall$$e$, ${\it e'}$:$E$.\+
\\[0ex]rcv?($e$) $\Rightarrow$ rcv?(${\it e'}$) $\Rightarrow$ link($e$) $=$ link(${\it e'}$) $\Rightarrow$ sender($e$) $<$ sender(${\it e'}$) $\Rightarrow$ $e$ $<$ ${\it e'}$)
\-\\[0ex]\& ($\forall$$e$:$E$. $\neg$first($e$) $\Rightarrow$ ($\forall$$x$:Id. ${\it when}$($x$,$e$) $=$ ${\it after}$($x$,pred($e$))))
\-\-
\end{tabbing}